Require Import AutoSep.

Definition array_swap (a:list W)(i j:W) :=
  let t := Array.sel a i in
    let a' := Array.upd a i (Array.sel a j) in
      Array.upd a' j t.

Definition allbool := List.Forall (fun w:W => w = 0 \/ w = 1).

Definition filter_eq (w:W) := List.filter (weqb w).

Definition swapS := SPEC("a", "i", "j") reserving 10
  Al ls,
  PRE[V] array ls (V "a") *
         [| (wordToNat (V "i") < length ls)%nat |] *
         [| (wordToNat (V "j") < length ls)%nat |]
  POST[_] array (array_swap ls (V "i") (V "j")) (V "a").

Definition sort_bool (ls:list W) := filter_eq 0 ls ++ filter_eq 1 ls.

Definition sortS := SPEC("a", "s") reserving 20
  Al ls,
  PRE[V] array ls (V "a") * [| wordToNat (V "s") = length ls |] * [| allbool ls |]
  POST[_] array (sort_bool ls) (V "a").
